#include "isop.h"

#define ALL1 0xFFFFFFFFFFFFFFFFULL
#define P0 0x5555555555555555ULL
#define P1 0x3333333333333333ULL
#define P2 0x0F0F0F0F0F0F0F0FULL
#define P3 0x00FF00FF00FF00FFULL
#define P4 0x0000FFFF0000FFFFULL
#define P5 0x00000000FFFFFFFFULL
#define N0 0xAAAAAAAAAAAAAAAAULL
#define N1 0xCCCCCCCCCCCCCCCCULL
#define N2 0xF0F0F0F0F0F0F0F0ULL
#define N3 0xFF00FF00FF00FF00ULL
#define N4 0xFFFF0000FFFF0000ULL
#define N5 0xFFFFFFFF00000000ULL

typedef ushort len_t;
typedef ushort var_t;

//=============================================================================
//      Static Function 
//=============================================================================
inline unsigned varsig(unsigned i ){return 1<<(i+i);}
// the 64 bit number for the operation 
static const uint64_t mask0[6] = {N0,N1,N2,N3,N4,N5};
static const uint64_t mask1[6] = {P0,P1,P2,P3,P4,P5};
// f-1(x) , which f(x) = 1<<(x-6), 
static const unsigned short mylog[33] ={ 0,6,7,0,8,0,0,0,  9,0,0,0,0,0,0,0, 10,0,0,0,0,0,0,0,  0,0,0,0,0,0,0,0, 11};
// 1<<x
static const unsigned short pow2[6] = {1,2,4,8,16,32}; // faster than inline function
static bool is0( len_t s , const bool_t f ) 
{
   for( unsigned i = 0 ; i<s ; ++ i )
      if( f[i] != 0 )return false;
   return true;
}
static bool is1( len_t s , const bool_t f )
{
   for( unsigned i = 0 ; i < s ; ++ i )
      if( f[i] != ALL1 ) return false;
   return true;
}
inline uint64_t cofactor0( var_t v , uint64_t u ){ u &= mask0[v]; return u | ( u>>pow2[v] ) ; }
inline uint64_t cofactor1( var_t v , uint64_t u ){ u &= mask1[v]; return u | ( u<<pow2[v] ) ; }
static bool large( len_t s , const bool_t a , const bool_t b )
{
   for(unsigned i = 0 ; i<s ;++i)
      if( (~a[i]) & (b[i]) ) return false;
   return true;
}
static void max_support( uint64_t a, uint64_t b , var_t & v )
{
   while( v > 0 )
   {
      if( ((a&mask0[v]) >> pow2[v] )!= (a&mask1[v]) ||  
          ((b&mask0[v]) >> pow2[v] )!= (b&mask1[v])) return;
      v-=1;
   }
}
static void max_support( const bool_t a , const bool_t b, len_t & h )
{
   while( h )
   {
      for( int i = 0 ;  i < h ; ++ i )
         if( a[ i ] != a[ i+h ] || b[i] != b[i+h] )return;
      h /= 2;
   }
}
inline void ITE( var_t v , uint64_t pos , uint64_t neg , uint64_t none , uint64_t & r )
{
   r = none | (pos & mask1[v]) | ( neg & mask0[v] );
}
static void ITE( len_t h, const bool_t pos, const bool_t neg , const bool_t none , bool_t r )
{
   for( unsigned i = 0 ; i < h ; ++ i )
      r[i]   = none[i] | pos[i] , 
      r[i+h] = none[i] | neg[i] ;
}
inline void minus( uint64_t a , uint64_t b, uint64_t & o )
{
   o = a & (~b);
}
static void minus( len_t s , const bool_t a , const bool_t b, bool_t o )
{
   for( unsigned i = 0  ; i < s ; ++ i ) 
      o[i] = a[i] & (~b[i]);
}
inline void minusOr( uint64_t a , uint64_t na , uint64_t b , uint64_t nb , uint64_t & o )
{
   o = (a&(~na)) | (b &(~nb));
}
static void minusOr( len_t s, const bool_t a , const bool_t na , const bool_t b , const bool_t nb , bool_t o ) 
{
   for( unsigned i = 0 ; i < s ; ++ i )
      o[i] = (a[i]&(~na[i])) | (b[i]&(~nb[i]));
}
inline void andTo( uint64_t a , uint64_t & o )
{
   o &= a;
}
static void andTo( len_t s , const bool_t a , bool_t o )
{
   for( unsigned i = 0 ; i < s ; ++ i )
      o[i] &= a[i];
}
static void andTo( len_t s , const bool_t a , const bool_t  b , bool_t o)
{
   for( unsigned i = 0 ; i < s ; ++ i )
      o[i] = a[i] & b[i];
}
//=============================================================================
//      TRUTH TABLE ALLOCATION 
//=============================================================================
void   ISOP::table_allocate( unsigned n )
{
   uint64_t * p = new uint64_t[ n * TABLE_SIZE ];   assert( p );
   _truth_table_pages.push( p );
   for( unsigned i = 0 ; i < n ; ++ i ) 
   {
      _tables.push( bool_t( p ) );
      p += TABLE_SIZE;
   }
}
bool_t ISOP::newTruth()
{
   if( _recycleList.size() )
      return _recycleList.data[ -- _recycleList.sz ];
   if( _fun_ptr == _tables.size() )
      table_allocate( _fun_ptr );
   return _tables[ _fun_ptr++ ];
}
bool_t ISOP::newTruth( uint64_t u )
{
   if( u == 0 )    return _tables[0];
   if( u == ALL1 ) return _tables[1];

   bool_t r = newTruth();
   r[0] = u;
   return r;
}
void ISOP::remove( bool_t b )
{
   if( b.isClone( _c0 ) ) return ;
   if( b.isClone( _c1 ) ) return ; // TODO because of c0,c1 are allocation in same time , could be optimize

   _recycleList.push( b );
}
inline void ISOP::merge( var_t v , sop_t a , sop_t b , sop_t & o )
{
   SopData sop ( v , a , b , o );
   o = _sops.size();
   _sops.push( sop );
}
//=============================================================================
//      MORREALE MINATO ALGORITHM
//=============================================================================
void ISOP::Morreale_Minato_ISOP( const bool_t f , const bool_t cf , var_t u ,  sop_t & sop , bool_t & of )
{
   unsigned short v = u;
   if( u != 0 )
   {
      if( is0( u<<1 , f ) ){ sop = 0 , of = _tables[0] ; return ; }
      if( is1( u<<1 ,cf ) ){ sop = 1 , of = _tables[1] ; return ; }
      max_support( f , cf , v ); // return v

      if( v != 0 ) Morreale_Minato_ISOP_core( f , cf  , v , sop , of );
   }

   if( v == 0 ) 
   {
      uint64_t o ;
      Morreale_Minato_ISOP( f[0] , cf[0] , 5 , sop , o );
      of = newTruth( o );
   }
  
   if( of.isClone( _c0 ) ) return;
   if( u == v ) return; 

   u+=u, v+=v?v:1; 
   for( unsigned i = v ; i < u ; i+= v)
      for( unsigned j = 0 ; j < v ; ++ j )
         of[i+j] = of[j];
}
void ISOP::Morreale_Minato_ISOP_core( const bool_t f , const bool_t cf , var_t v ,  sop_t & sop , bool_t & of )
{
   const bool_t f0 = f.neg(v) ,f1 = f , 
               cf0 = cf.neg(v) ,cf1 = cf;

   bool_t tmp = newTruth();
   bool_t ret0 , ret1 , ret2 ;

   sop_t sop0, sop1;

   minus( v , f0 , cf1 , tmp );
   Morreale_Minato_ISOP( tmp , cf0 , v/2 , sop0 , ret0 ); 

   minus( v, f1 , cf0 , tmp );
   Morreale_Minato_ISOP( tmp , cf1 , v/2 , sop1 , ret1 );

   bool_t qcf = newTruth(); 
   andTo( v , cf0 , cf1 , qcf );
   minusOr( v , f0 , ret0 , f1 , ret1 , tmp );
   Morreale_Minato_ISOP( tmp , qcf , v/2 , sop , ret2 );
   
   merge( ::mylog[v] , sop1 , sop0 , sop );

   if( ret0.isClone( _c0 ) && ret1.isClone( _c0 ) ) 
   {
      remove( tmp );
      tmp = ret2;

      if( ! tmp.isClone(_c0) ) 
      for( unsigned i = 0 ; i < v ; ++ i )
         tmp[i+v] = ret2[i];
   }
   else
   {
      ITE( v , ret1 , ret0 , ret2 , tmp );
      remove( ret2 );
   }
   remove( ret0 ), remove( ret1 ) , remove( qcf );
   of = tmp; 
}
void ISOP::Morreale_Minato_ISOP( uint64_t f , uint64_t cf , var_t v , sop_t & sop , uint64_t & of )
{
   uint64_t f0 , f1 , cf0 , cf1 , tmp , ret0 , ret1 , ret2 ;
   sop_t sop0, sop1;

   if( f == 0 )  { of = 0 ;  sop = 0 ; return;}
   if( cf == ALL1  ){ of = cf; sop = 1 ; return;}

   max_support( f , cf , v ); // return v
     
   f0 = cofactor0( v , f ), cf0 = cofactor0( v , cf ),  cf1 = cofactor1( v , cf );
   minus( f0 , cf1 , tmp );
   Morreale_Minato_ISOP( tmp , cf0 , v-1 , sop0 , ret0 ); 

   f1 = cofactor1( v , f );
   minus( f1 , cf0 , tmp );
   Morreale_Minato_ISOP( tmp , cf1 , v-1 , sop1 , ret1 );

   minusOr( f0 , ret0 , f1 , ret1 , tmp );//tmp = (f0 - ret0) | (f1-ret1); 
   andTo( cf1 , cf0 );              //cf0 &= cf1;
   Morreale_Minato_ISOP( tmp , cf0 , v-1 , sop , ret2 );

   merge(v,sop1,sop0,sop);
   ITE( v , ret1 , ret0 , ret2 , tmp );
   of = tmp;
}
unsigned ISOP::build_cube( unsigned * mem )
{
   sop_t idx = _sops.size()-1;
   
   unsigned k = 0;
   while( idx > 1 ) 
   {
      if( k > RF_MAX_SOP_SIZE )return RF_MAX_SOP_SIZE;
      SopData sop = _sops[idx--];
      unsigned v = varsig(sop.var);

      if( sop.pos > 1 ) _sops[ sop.pos ].cube = v | sop.cube;
      else if ( sop.pos == 1 )mem[k++] = v | sop.cube;

      v += v;
      if( sop.neg > 1 ) _sops[ sop.neg ].cube = v | sop.cube;
      else if ( sop.neg == 1 ) mem[k++] = v | sop.cube;

      if( sop.none > 1 ) _sops[ sop.none ].cube = sop.cube; 
      else if( sop.none == 1 ) mem[k++] = sop.cube; 
   }
   return k;
}
unsigned ISOP::Morreale_Minato_ISOP( const bool_t f, const bool_t cf , var_t v , unsigned * mem )
{
   sop_t sop; bool_t ret;

   _sops.downTo(2) ;     // sop clear
   _recycleList.clear(); // table clear 
   _fun_ptr = 2 ;

   Morreale_Minato_ISOP( f , cf , v , sop , ret );
   return build_cube( mem );
}
//=============================================================================
//      CONSTRUCTOR AND DESTRUCTOR
//=============================================================================
ISOP::ISOP()
{
   //--- truth_table allocation 
   table_allocate( 128 ); //

   for( int i = 0 ; i < TABLE_SIZE ; ++ i )
      _tables[0][i] = 0 , _tables[1][i] = ALL1; // Could be modify as memset 

   _c0 = _tables[0];
   _c1 = _tables[1];

   _sops.push(); // 0 and 1 are special nodes
   _sops.push();
}
ISOP::~ISOP()
{
   for( unsigned i = 0 ; i < _truth_table_pages.size() ; ++ i ) 
      delete [] _truth_table_pages[i];
}

